//
//$Id: min_kw.cpp 687 2011-03-13 12:21:29Z andrew.tsyganov $
#include "stdafx.h"
#include <numeric>
#include "include/min_kw.h"
#include "include/utils.h"
#include "include/fa_utils.h"
#include "include/combgen.h"
#include "include/my_time.h"
#include "include/sets.h"
#include "contrib/rapidxml/rapidxml.hpp"
#include <algorithm>

using namespace std;
using namespace kw;
using namespace rapidxml;

void KW_Parameters::init_Default()
{
    solver_         = kKWStateExact;
    //solver_         = kKWStateGA;
    //solver_         = kKWStateSA;
    verbosity_      = 1;
    find_all_       = true;

    min_cover_size_ = 0;
    max_cover_size_ = 0;

    sa_xml_         = kKWSAXml;
    ga_xml_         = kKWGAXml;
    shc_xml_        = kKWSHCXml;

    symbols_pfx_    = kKWSymbolsPfx;
    a_pfx_          = kKWAPfx;
    da_pfx_         = kKWDAPfx;
    dra_pfx_        = kKWDRAPfx;
    mda_pfx_        = kKWMDAPfx;
    mdra_pfx_       = kKWMDRAPfx;
    imda_pfx_       = kKWIMDAPfx;
}

void KW_Parameters::print_TXT(std::ostream& os) const
{
    os << "KW_Parameters:" << endl;
    os << "solver = " << solver_ << endl;
    os << "verbosity = " << verbosity_ << endl;
    os << "find_all = " << (find_all_ ? "true" : "false") << endl;
    os << "min_cover_size = " << min_cover_size_ << endl;
    os << "max_cover_size = " << max_cover_size_ << endl;
    os << "ga_xml = " << ga_xml_ << endl;
    os << "sa_xml = " << sa_xml_ << endl;
    os << "shc_xml = " << shc_xml_ << endl;
    os << "symbols_pfx = " << symbols_pfx_ << endl;
    os << "a_pfx = " << a_pfx_ << endl;
    os << "da_pfx = " << da_pfx_ << endl;
    os << "dra_pfx = " << dra_pfx_ << endl;
    os << "mda_pfx = " << mda_pfx_ << endl;
    os << "mdra_pfx = " << mdra_pfx_ << endl;
    os << "imda_pfx = " << imda_pfx_ << endl;
}

bool KW_Parameters::load_XML(string const& file)
{
    init_Default();

    vector<char> buffer;
    xml_document<> doc;
    xml_node<>* node;
    xml_node<>* kw_node;
    xml_node<>* pfx_node;

    // process min_kw node
    kw_node = GetNode(file, buffer, doc, kKWXmlNode);
    if (kw_node == NULL)
    {
        cout << "KW_Parameters::load_XML error: '" << kKWXmlNode << "' node is missing!" << endl;
        return false;
    }

    // process solver node 
    node = kw_node->first_node(kKWXmlSolverNode.c_str(), 0, false);
    if (node != NULL)
    {
        string s = ToLower(node->value());

        if ((s == kKWStateExact) || (s == kKWStateGA) || (s == kKWStateSA) || (s == kKWStateSHC))
        {
            solver_ = s;
        }
        else
        {
            cout << "KW_Parameters::load_XML warning: wrong '" << kKWXmlSolverNode << "' node value. Using default!" << endl;
        }
    }

    // process verbosity node 
    node = kw_node->first_node(kKWXmlVerbosityNode.c_str(), 0, false);
    if (node != NULL)
    {
        int val = atoi(node->value());

        if ((val >= 0) && (val <= 2))
        {
            verbosity_ = val;
        }
        else
        {
            cout << "KW_Parameters::load_XML warning: wrong '" << kKWXmlVerbosityNode << "' node value. Using default!" << endl;
        }
    }

    // process find_all node 
    node = kw_node->first_node(kKWXmlFindAllNode.c_str(), 0, false);
    if (node != NULL)
    {
        string s = ToLower(node->value());

        if ((s == "true") || (s == "yes") || (s == "") || (s == "no"))
        {
            find_all_ = ((s == "true") || (s == "yes") ? true : false);
        }
        else
        {
            cout << "KW_Parameters::load_XML warning: wrong '" << kKWXmlFindAllNode << "' node value. Using default!" << endl;
        }
    }

    // process min_cover_size node 
    node = kw_node->first_node(kKWXmlMinCoverSizeNode.c_str(), 0, false);
    if (node != NULL)
    {
        int val = atoi(node->value());

        if (val >= 0)
        {
            min_cover_size_ = val;
        }
        else
        {
            cout << "KW_Parameters::load_XML warning: wrong '" << kKWXmlMinCoverSizeNode << "' node value. Using default!" << endl;
        }
    }

    // process max_cover_size node 
    node = kw_node->first_node(kKWXmlMaxCoverSizeNode.c_str(), 0, false);
    if (node != NULL)
    {
        int val = atoi(node->value());

        if (val >= 0)
        {
            max_cover_size_ = val;
        }
        else
        {
            cout << "KW_Parameters::load_XML warning: wrong '" << kKWXmlMaxCoverSizeNode << "' node value. Using default!" << endl;
        }
    }

    // process ga_xml node 
    node = kw_node->first_node(kKWXmlGAXmlNode.c_str(), 0, false);
    if (node != NULL)
    {
        ga_xml_ = node->value();
    }

    // process sa_xml node 
    node = kw_node->first_node(kKWXmlSAXmlNode.c_str(), 0, false);
    if (node != NULL)
    {
        sa_xml_ = node->value();
    }

    // process shc_xml node 
    node = kw_node->first_node(kKWXmlSHCXmlNode.c_str(), 0, false);
    if (node != NULL)
    {
        shc_xml_ = node->value();
    }

    // process prefixes node 
    pfx_node = kw_node->first_node(kKWXmlPrefixesNode.c_str(), 0, false);

    if (pfx_node != NULL)
    {
        // process symbols node 
        node = pfx_node->first_node(kKWXmlSymbolsNode.c_str(), 0, false);
        if (node != NULL)
        {
            symbols_pfx_ = node->value();
        }

        // process a node 
        node = pfx_node->first_node(kKWXmlANode.c_str(), 0, false);
        if (node != NULL)
        {
            a_pfx_ = node->value();
        }

        // process da node 
        node = pfx_node->first_node(kKWXmlDANode.c_str(), 0, false);
        if (node != NULL)
        {
            da_pfx_ = node->value();
        }

        // process dra node 
        node = pfx_node->first_node(kKWXmlDRANode.c_str(), 0, false);
        if (node != NULL)
        {
            dra_pfx_ = node->value();
        }

        // process mda node 
        node = pfx_node->first_node(kKWXmlMDANode.c_str(), 0, false);
        if (node != NULL)
        {
            mda_pfx_ = node->value();
        }

        // process mdra node 
        node = pfx_node->first_node(kKWXmlMDRANode.c_str(), 0, false);
        if (node != NULL)
        {
            mdra_pfx_ = node->value();
        }

        // process imda node 
        node = pfx_node->first_node(kKWXmlIMDANode.c_str(), 0, false);
        if (node != NULL)
        {
            imda_pfx_ = node->value();
        }
    }

    return true;
}

KW_Statistics::KW_Statistics()
{
    d_.resize(kDKWStatNum);
    u_.resize(kUKWStatNum);
    b_.resize(kBKWStatNum);
}

void KW_Statistics::reset()
{
    iterations_time_.clear();
    fill(d_.begin(), d_.end(), 0);
    fill(u_.begin(), u_.end(), 0);
    fill(b_.begin(), b_.end(), false);
}

void Min_KW::clear()
{
    ra_.clear();
    da_.clear();
    dra_.clear();
    mda_.clear();
    mdra_.clear();
    
    vs_a_.clear();
    vs_ra_.clear();
    vs_da_.clear();
    vs_dra_.clear();
    
    ram_.clear();

    grids_.clear();
    v_min_.clear();

    stat_.reset();
}

void Min_KW::build_RA()
{
    double start_time = get_time();

    Reverse(a_, ra_);
    
    double end_time = get_time();

    stat_.d_[RA_TIME] = end_time - start_time;
    stat_.d_[TOTAL_TIME] += stat_.d_[RA_TIME];
}

void Min_KW::build_DA()
{
    double start_time = get_time();
    
    Determinize(a_, da_, vs_a_);
    
    u_t n = vs_a_.size();
    u_t empty_id = FindEmptySet(vs_a_);
    if (empty_id != n)
    {
        da_.swap_States(empty_id, n - 1);
        swap(vs_a_[empty_id], vs_a_[n - 1]);
    }
    
    double end_time = get_time();

    stat_.u_[DA_STATES] = da_.get_States_Num();
    stat_.d_[DA_TIME] = end_time - start_time;
    stat_.d_[TOTAL_TIME] += stat_.d_[DA_TIME];
}

void Min_KW::build_DRA()
{
    double start_time = get_time();

    Determinize(ra_, dra_, vs_ra_);

    u_t n = vs_ra_.size();
    u_t empty_id = FindEmptySet(vs_ra_);
    if (empty_id != n)
    {
        dra_.swap_States(empty_id, n - 1);
        swap(vs_ra_[empty_id], vs_ra_[n - 1]);
    }

    double end_time = get_time();

    stat_.u_[DRA_STATES] = dra_.get_States_Num();
    stat_.d_[DRA_TIME] = end_time - start_time;
    stat_.d_[TOTAL_TIME] += stat_.d_[DRA_TIME];
}

void Min_KW::build_MDA()
{
    double start_time = get_time();

    FA rda;
    Reverse(da_, rda);
    MinimizeHopcroft(da_, rda, mda_, vs_da_);

    u_t n = vs_da_.size();
    nes_num_da_ = n;
    u_t empty_id = FindEmptySet(vs_da_, vs_a_);
    if (empty_id != n)
    {
        --nes_num_da_;
        mda_.swap_States(empty_id, n - 1);
        swap(vs_da_[empty_id], vs_da_[n - 1]);
    }

    double end_time = get_time();

    stat_.u_[MDA_STATES] = mda_.get_States_Num();
    stat_.d_[MDA_TIME] = end_time - start_time;
    stat_.d_[TOTAL_TIME] += stat_.d_[MDA_TIME];
}

void Min_KW::build_MDRA()
{
    double start_time = get_time();

    FA rdra;
    Reverse(dra_, rdra);
    MinimizeHopcroft(dra_, rdra, mdra_, vs_dra_);

    u_t n = vs_dra_.size();
    nes_num_dra_ = n;
    u_t empty_id = FindEmptySet(vs_dra_, vs_ra_);
    if (empty_id != n)
    {
        --nes_num_dra_;
        mdra_.swap_States(empty_id, n - 1);
        swap(vs_dra_[empty_id], vs_dra_[n - 1]);
    }

    double end_time = get_time();

    stat_.u_[MDRA_STATES] = mdra_.get_States_Num();
    stat_.d_[MDRA_TIME] = end_time - start_time;
    stat_.d_[TOTAL_TIME] += stat_.d_[MDRA_TIME];
}

void Min_KW::build_RAM()
{
    double start_time = get_time();

    u_t m = nes_num_da_;
    u_t n = nes_num_dra_;
    
    vector<Subset> vs_r(m), vs_c(n);

    for (u_t i = 0; i < m; ++i)
    {
        for (Subset::const_iterator it = vs_da_[i].begin(); it != vs_da_[i].end(); ++it)
        {
            vs_r[i] |= vs_a_[*it];
        }
    }

    for (u_t j = 0; j < n; ++j)
    {
        for (Subset::const_iterator it = vs_dra_[j].begin(); it != vs_dra_[j].end(); ++it)
        {
            vs_c[j] |= vs_ra_[*it];
        }
    }

    ram_.init(m, n);
    for (u_t i = 0; i < m; ++i)
    {
        for (u_t j = 0; j < n; ++j)
        {
            Subset s = vs_r[i];
            s &= vs_c[j];
            
            if (!s.empty())
            {
                ram_.set(i, j);
            }
            else
            {
                ram_.reset(i, j);
            }
       }
    }

    double end_time = get_time();

    stat_.d_[RAM_TIME] = end_time - start_time;
    stat_.d_[TOTAL_TIME] += stat_.d_[RAM_TIME];

    stat_.u_[RAM_ROWS]       = m;
    stat_.u_[RAM_COLUMNS]    = n;
    stat_.u_[RAM_ONES_COUNT] = ram_.nones_;
    stat_.u_[RAM_SIZE] = m * n;
    stat_.d_[RAM_ONES_DENSITY] = ((double) ram_.nones_) / ( (double) m * n);
}

void Min_KW::determine_Cover_Size_Range()
{
    u_t min_size = max(stat_.u_[FIXED_COUNT], (u_t) ceil(log2((double) mda_.get_States_Num()))); //!!!
    u_t max_size = min(min(a_.get_States_Num() - 1, mda_.get_States_Num() - 1), stat_.u_[GRIDS_COUNT]); //!!!

    if (param_.verbosity_)
    {
        cout << endl
             << "Determining limits for covers search..." << endl
             << endl
             << "Number of fixed grids (A): " << stat_.u_[FIXED_COUNT] << endl
             << "Number of states in canonical automaton (B): " << mda_.get_States_Num() << endl
             << "Minimum cover size is MAX(A, Log2(B)): " << min_size << endl
             << endl
             << "Number of states in automaton (C): " << a_.get_States_Num() << endl
             << "Number of states in canonical automaton (D): " << mda_.get_States_Num() << endl
             << "Number of grids (E): " << stat_.u_[GRIDS_COUNT] << endl
             << "Maximium cover size is MIN(C-1, D-1, E): " << max_size << endl
             << endl;
    }

    bool min_user_defined = false;
    bool max_user_defined = false;

    if (param_.solver_ != "state_exact")
    {
        stat_.u_[MIN_COVER_SIZE] = min_size;
        stat_.u_[MAX_COVER_SIZE] = max_size;
    }
    else
    {
        if (param_.min_cover_size_ > 0)
        {
            if ((param_.min_cover_size_ < min_size) || (param_.min_cover_size_ > max_size))
            {
                if (param_.verbosity_)
                {
                    cout << endl
                         << "Warning: minimum cover size defined by user is out of range!!!" << endl;
                }

                stat_.u_[MIN_COVER_SIZE] = min_size;
            }
            else
            {
                stat_.u_[MIN_COVER_SIZE] = param_.min_cover_size_;
                min_user_defined = true;
            }
        }
        else
        {
            stat_.u_[MIN_COVER_SIZE] = min_size; 
        }
        
        if (param_.max_cover_size_ > 0)
        {
            if ((param_.max_cover_size_ < min_size) || (param_.max_cover_size_ > max_size))
            {
                if (param_.verbosity_)
                {
                    cout << endl
                         << "Warning: maximum cover size defined by user is out of range!!!" << endl;
                }

                stat_.u_[MAX_COVER_SIZE] = max_size;
            }
            else
            {
                stat_.u_[MAX_COVER_SIZE] = param_.max_cover_size_;
                max_user_defined = true;
            }
        }
        else
        {
            stat_.u_[MAX_COVER_SIZE] = max_size; 
        }
    }

    if (param_.verbosity_)
    {
        cout << endl
             << "Minimum cover size: " << stat_.u_[MIN_COVER_SIZE] << (min_user_defined ? " (user defined)" : " (determined automatically)") << endl
             << "Maximum cover size: " << stat_.u_[MAX_COVER_SIZE] << (max_user_defined ? " (user defined)" : " (determined automatically)") << endl;
        
        if (stat_.u_[MAX_COVER_SIZE] < stat_.u_[MIN_COVER_SIZE])
        {
            cout << endl
                 << "Warning: maximum cover size is less then minimum cover size!!!" << endl;
        }
    }
}

bool Min_KW::do_Iteration_SEQ(u_t const m)
{
    if (param_.verbosity_)
    {
        cout << endl 
             << ">>> Searching for covers of size " << stat_.u_[FIXED_COUNT] + m << endl;
    }

    double start_time = get_time();

    Subset_Matrix cm;
    Bool_Matrix   hits;
    FA imda;
    vector<Subset> vs_sa;
    Subset s;
    CombGen cgen;

    u_t n = stat_.u_[GRIDS_COUNT] - stat_.u_[FIXED_COUNT]; // !!!

    cm.init(stat_.u_[RAM_ROWS], stat_.u_[RAM_COLUMNS]);
    hits.init(stat_.u_[RAM_ROWS], stat_.u_[RAM_COLUMNS]);

    bool covers_found = false;
    bool min_found  = false;

    cgen.init(m, n, s); // generate the first subset of grids
    do
    {
        hits = ram_;
        for (Subset::const_iterator it = s.begin(); it != s.end(); ++it)
        {
            hits.cover(grids_[stat_.u_[FIXED_COUNT] + *it]);
        }

        if (hits.nones_ == 0) // if the subset of grids is a cover
        {
            covers_found = true;

            if (param_.verbosity_)
            {
                cout << endl 
                     << "<<< Cover of size " << stat_.u_[FIXED_COUNT] + m << " found" << endl;

                output_Cover(cout, s);

                cout << endl 
                     << ">>> Testing legitimacy of the cover..." << endl;
            }

            make_Subset_Assignment(s, cm, vs_sa); // assign subsets

            if (param_.verbosity_)
            {
                output_CM(cout, cm);
            }

            apply_Intersection_Rule(vs_sa, stat_.u_[FIXED_COUNT] + m, imda); // apply intesection rule
            //output_FA(cout, imda, kDefaultLabelsPfx);

            if (is_Equivalent_FA(imda)) // check if the constructed automaton is equivalent to the original
            {
                if (param_.verbosity_)
                {
                    cout << endl 
                         << "<<< Cover is legitimate" << endl;
                }

                min_found = true;
                v_min_.push_back(imda);
                v_min_[stat_.u_[MIN_COUNT]].set_Name(a_.get_Name() + "_min_" + IntToString(stat_.u_[MIN_COUNT]));
                ++stat_.u_[MIN_COUNT];

                if (!param_.find_all_) 
                    break;
            }
            else
            {
                if (param_.verbosity_)
                {
                    cout << endl 
                         << "<<< Cover is not legitimate!!!" << endl;
                }
            }
        }
    }
    while (!cgen.next(s)); // generate the next subset of grids

    double end_time = get_time();

    stat_.iterations_time_.push_back(end_time - start_time);
    stat_.d_[SEARCH_TIME] += stat_.iterations_time_.back();
    stat_.d_[TOTAL_TIME]  += stat_.iterations_time_.back();

    if (min_found) 
    {
        stat_.u_[MIN_STATES] = stat_.u_[FIXED_COUNT] + m;
    }

    if (!min_found && covers_found)
    {
        stat_.b_[ILLEG_MIN_COVERS] = true;
    }

    if (param_.verbosity_)
    {
        if (!covers_found)
        {
            cout << "<<< Covers not found!!!" << endl;
        }

        cout << endl
             << "iteration time = " << stat_.iterations_time_.back() << " s" << endl;
    }

    return min_found;
}

bool Min_KW::is_Equivalent_FA(FA const& imda, int const method) const
{
    if (method == 0)
    {
        FA mdimda;
        vector<u_t> vu;

        MinimizeBrzozowski(imda, mdimda);
        //mdimda.print_TXT(cout);

        return AreIsomorphicDFAs(mda_, mdimda, vu);
    }
    else
    {
        FA dimda;
        vector<Subset> vs_imda;

        Determinize(imda, dimda, vs_imda);

        return AreEquivalentDFAs(mda_, dimda);
    }
}

void Min_KW::make_Subset_Assignment(Subset const& s, Subset_Matrix& cm, std::vector<Subset>& vs_sa) const
{
    //cm = cm_;
	cm.clear();
    u_t n = stat_.u_[FIXED_COUNT];

    for (u_t i = 0; i < n; ++i)
    {
        cm.cover(grids_[i], i);
    }

    for (Subset::const_iterator it = s.begin(); it != s.end(); ++it)
    {
		//cout << "n = " << n << " *it = " << *it << " Grid = " << grids_[stat_.u_[FIXED_COUNT] + *it].to_String() << endl;
        cm.cover(grids_[stat_.u_[FIXED_COUNT] + *it], n);
		//output_CM(cout, cm);
        ++n;
    }

    vs_sa.clear();
    u_t m = mda_.get_States_Num();
    vs_sa.resize(m);

    for (u_t i = 0; i < cm.size(); ++i)
    {
        for (u_t j = 0; j < cm[i].size(); ++j)
        {
            vs_sa[i] |= cm[i][j];
        }
    }

    //debug 
    //for (u_t i = 0; i < vs_sa.size(); ++i)
    //    cout << vs_sa[i].to_String() << endl;
}

void Min_KW::apply_Intersection_Rule(std::vector<Subset> const& vs_sa, size_t const n, FA& imda) const
{
    u_t m = mda_.get_Symbols_Num(); 
    vector<Adjacent> const& mda_delta = mda_.get_Delta();

    imda.init("ir(" + mda_.get_Name() + ")", m, n);
    imda.set_Symbols(mda_.get_Symbols()); 

    // build a transition function
    for (u_t i = 0; i < n; ++i) // for each state of the automaton being constructed
    {
        vector<u_t> v_src; // v_src - vector of state IDs for which assigned subsets contain i
        v_src.reserve(vs_sa.size());

        for (u_t k = 0; k < vs_sa.size(); ++k) // for each assigned subset
        {
            if (vs_sa[k].contains(i)) // if the current state is contained in a subset assigned to the k-th state of the original DFA
            {
                v_src.push_back(k); // remember this (k-th) state
            }
        }
        
        for (u_t j = 0; j < m; ++j) // for each symbol of the alphabet
        { 
            vector<u_t> v_dst; // v_dst - vector of state IDs to which there is a transition from v_src by symbol j 
            v_dst.resize(v_src.size());

            for (u_t k = 0; k < v_src.size(); ++k) // for each remembered state
            {
                v_dst[k] = *(mda_delta[v_src[k]].get_Dst(j).begin()); // remember the state to which there is a transition by the current symbol
            }

            // using the intersection rule construct a set s such that delta(i,j) = s
            Subset s;
            if (!v_dst.empty()) // TODO: is it possible?
            {
                s = vs_sa[v_dst[0]];
                for (u_t k = 1; k < v_dst.size(); ++k) 
                {
                    s &= vs_sa[v_dst[k]];
                }
            }

            //cout << "ir: s = " << s.to_String() << endl;
            // add transitions from the i-th state by the j-th symbol to all states of s
            imda.add_Transitions(i, j, s);
        }
    }
        
    // mark initial states
    u_t state_id = *(mda_.get_Initial().begin()); // remember ID of the initial state of the original automaton
    ASSERT_(state_id >= 0);

    for (Subset::const_iterator it = vs_sa[state_id].begin(); it != vs_sa[state_id].end(); ++it) // for each elements of the subset assigned to it
    {
        imda.set_Initial(*it);   // mark the corresponding state as initial in the automaton being constructed
    }

    // mark final states
    for (u_t i = 0; i < n; ++i) // for each state of the automaton being constructed
    {
        // if the state is contained only in subsets assigned to final states of the original DFA
        bool found_in_nonfinal = false;
        for (u_t j = 0; j < vs_sa.size(); ++j)
        {
            if (vs_sa[j].contains(i) && !mda_.is_Final(j))
            {
                found_in_nonfinal = true;
            }
        }

        // mark this state as final
        if (!found_in_nonfinal)
        {
            imda.set_Final(i);
        }
    }
}

/* ================================================================================= */
/* Printing and output routines                                                      */
/* ================================================================================= */

void Min_KW::print_RAM_TXT(std::ostream& os) const
{
    u_t m = nes_num_da_;
    u_t n = nes_num_dra_;

    // determine maximum width of columns
    u_t max_left_width;
    vector<u_t> max_columns_width(n);

    max_left_width = 0;
    for (u_t i = 0; i < m; ++i)
    {
        u_t len = mda_.state_To_String(i, param_.mda_pfx_).length();
        if (len > max_left_width)
        {
            max_left_width = len;
        }
    }

    for (u_t j = 0; j < n; ++j)
    {
        max_columns_width[j] = mdra_.state_To_String(j, param_.mdra_pfx_).length();
    }

    // total width of the table
    u_t total_width = accumulate(max_columns_width.begin(), max_columns_width.end(), 4 + max_left_width + 3 * n);

    // print horizontal line
    PrintLine(os, total_width);

    // print table's header
    os << "|" << setw((streamsize) max_left_width + 3) << " |";
    for (u_t j = 0; j < n; ++j)
    {
        os << setw((streamsize) max_columns_width[j] + 1) << mdra_.state_To_String(j, param_.mdra_pfx_) << " |";
    }
    os << endl;

    // print horizontal line
    PrintLine(os, total_width);

    // print table
    for (u_t i = 0; i < m; ++i)
    {
        // print leftmost column
        os << "| " << setw((streamsize) max_left_width) << mda_.state_To_String(i, param_.mda_pfx_) << " |";
        // print matrix
        for (u_t j = 0; j < n; ++j)
        {
            os << setw((streamsize) max_columns_width[j] + 1) << (ram_[i][j] ? "1" : "0") << " |";
        }
        os << endl;
    }

    // print horizontal line
    PrintLine(os, total_width);
}    

void Min_KW::print_RAM_LaTeX(ostream& os) const
{
    u_t m = nes_num_da_;
    u_t n = nes_num_dra_;

    os << "\\begin{tabular}{|r||";

    for (u_t j = 0; j < n; ++j)
    {
        os << "c|";
    }
    
    os << "}" << endl
       << "\\hline" << endl
       << " & ";

    for (u_t j = 0; j < n; ++j)
    {
        os << mdra_.state_To_String(j, param_.mdra_pfx_, LATEX) << (j < n - 1 ? " & " : " \\\\\n");
    }

    os << "\\hline" << endl
       << "\\hline" << endl;

    for (u_t i = 0; i < m; ++i)
    {
        os << mdra_.state_To_String(i, param_.mdra_pfx_, LATEX) << " & ";

        for (u_t j = 0; j < n; ++j)
        {
            os << (ram_[i][j] ? "1" : "0") << (j < n - 1 ? " & " : " \\\\\n");
        }

        os << "\\hline" << endl;
    }

    os << "\\end{tabular}" << endl;
}

void Min_KW::print_CM_TXT(std::ostream& os, Subset_Matrix const& cm) const
{
    u_t m = nes_num_da_;
    u_t n = nes_num_dra_;

    // determine maximum width of columns
    u_t max_left_width;
    vector<u_t> max_columns_width(n);

    max_left_width = 0;
    for (u_t i = 0; i < m; ++i)
    {
        u_t len = mda_.state_To_String(i, param_.mda_pfx_).length();
        if (len > max_left_width)
        {
            max_left_width = len;
        }
    }

    for (u_t j = 0; j < n; ++j)
    {
        max_columns_width[j] = mdra_.state_To_String(j, param_.mdra_pfx_).length();
    }

    for (u_t j = 0; j < n; ++j)
    {
        for (u_t i = 0; i < m; ++i)
        {
            u_t len = cm[i][j].to_String().length();
            if (len > max_columns_width[j])
            {
                max_columns_width[j] = len;
            }
        }
    }

    // total width of the table
    u_t total_width = accumulate(max_columns_width.begin(), max_columns_width.end(), 4 + max_left_width + 3 * n);

    // print horizontal line
    PrintLine(os, total_width);

    // print table's header
    os << "|" << setw((streamsize) max_left_width + 3) << " |";
    for (u_t j = 0; j < n; ++j)
    {
        os << setw((streamsize) max_columns_width[j] + 1) << mdra_.state_To_String(j, param_.mdra_pfx_) << " |";
    }
    os << endl;

    // print horizontal line
    PrintLine(os, total_width);

    // print table
    for (u_t i = 0; i < m; ++i)
    {
        // print leftmost column
        os << "| " << setw((streamsize) max_left_width) << mda_.state_To_String(i, param_.mda_pfx_) << " |";
        // print matrix
        for (u_t j = 0; j < n; ++j)
        {
            os << setw((streamsize) max_columns_width[j] + 1) << cm[i][j].to_String() << " |";
        }
        os << endl;
    }

    // print horizontal line
    PrintLine(os, total_width);
}

void Min_KW::print_CM_LaTeX(std::ostream& os, Subset_Matrix const& cm) const
{
    u_t m = nes_num_da_;
    u_t n = nes_num_dra_;

    os << "\\begin{tabular}{|r||";

    for (u_t j = 0; j < n; ++j)
    {
        os << "c|";
    }
    
    os << "}" << endl
       << "\\hline" << endl
       << " & ";

    for (u_t j = 0; j < n; ++j)
    {
        os << mdra_.state_To_String(j, param_.mdra_pfx_, LATEX) << (j < n - 1 ? " & " : " \\\\\n");
    }

    os << "\\hline" << endl
       << "\\hline" << endl;

    for (u_t i = 0; i < m; ++i)
    {
        os << mda_.state_To_String(i, param_.mda_pfx_, LATEX) << " & ";

        for (u_t j = 0; j < n; ++j)
        {
            os << (cm[i][j].empty() ? "" : cm[i][j].to_String(LATEX_BRACES)) << (j < n - 1 ? " & " : " \\\\\n");
        }

        os << "\\hline" << endl;
    }

    os << "\\end{tabular}" << endl;
}

void Min_KW::print_Grids_Set_TXT(ostream& os, Subset const& s) const
{
    string fixed_marker = "* ";
    string var_marker   = "  ";

    u_t marker_space = (stat_.u_[FIXED_COUNT] > 0 ? fixed_marker.length() + 1 : 0);
    u_t w = (s.size() > 0 ? Width(stat_.u_[FIXED_COUNT] + s.size() - 1) : 0);

    u_t k = 0;
    
    for (u_t i = 0; i < stat_.u_[FIXED_COUNT]; ++i)
    {
        os << fixed_marker << setw((streamsize) w) << k << ") " << grids_[i].to_String() << endl;
        ++k;
    }
    
    for (Subset::const_iterator it = s.begin(); it != s.end(); ++it)
    {
        os << var_marker << setw((streamsize) w) << k << ") " << grids_[stat_.u_[FIXED_COUNT] + *it].to_String() << endl;
        ++k;
    }
}

void Min_KW::print_Grids_Set_LaTeX(ostream& os, Subset const& s) const
{
    string fixed_marker = "*\\ ";
    string var_marker   = "\\ \\ ";

    os << "\\begin{itemize}" << endl;

    u_t k = 0;

    for (u_t i = 0; i < stat_.u_[FIXED_COUNT]; ++i)
    {
        os << "\\item[" << fixed_marker << k << ")] " << grids_[i].to_String(LATEX_BRACES) << endl;
        ++k;
    }
    
   for (Subset::const_iterator it = s.begin(); it != s.end(); ++it)
    {
        os << "\\item[" << k << ")] " << grids_[stat_.u_[FIXED_COUNT] + *it].to_String(LATEX_BRACES) << endl;
        ++k;
    }

    os << "\\end{itemize}" << endl;
}

void Min_KW::output_FA(ostream& os, FA const& a, Labels_Prefix const& lp, double const time) const
{
    os << endl;
    a.print_TXT(os, lp);

    if (param_.verbosity_ > 1)
    {
        os << endl
           << "GAP:" << endl
           << a.to_GAP() << endl;

        os << endl
           << "LaTeX:" << endl;
        a.print_LaTeX(os, lp);

        os << endl
           << "Graphviz:" << endl;
        a.print_GV(os, lp);
    }

    if (time >= 0)
    {
        os << endl
           << "time = " << time << " s" << endl;
    }
}

void Min_KW::output_DFA(ostream& os, FA const& da, FA const& a, vector<Subset> const& vs_a, Labels_Prefix const& lp_da, Labels_Prefix const& lp_a, double const time) const
{
    os << endl;
    da.print_TXT(os, a, vs_a, lp_a, lp_da);

    if (param_.verbosity_ > 1)
    {
        os << endl
           << "GAP:" << endl
           << da.to_GAP() << endl;

        os << endl
           << "LaTeX:" << endl;
        da.print_LaTeX(os, a, vs_a, lp_a, lp_da);

        os << endl
           << "Graphviz:" << endl;
        da.print_GV(os, lp_a);
    }

    if (time >= 0)
    {
        os << endl
           << "time = " << time << " s" << endl;
    }
}

void Min_KW::output_Grids(ostream& os) const
{
    Subset var;
    
    if (stat_.u_[GRIDS_COUNT] > stat_.u_[FIXED_COUNT])
    {
        var.insert_range(0, stat_.u_[GRIDS_COUNT] - stat_.u_[FIXED_COUNT] - 1);
    }

    print_Grids_Set_TXT(os, var);

    if (param_.verbosity_ > 1)
    {
        os << endl
           << "LaTeX:" << endl;
        print_Grids_Set_LaTeX(os, var);
    }

    os << endl
       << "time = " << stat_.d_[GRIDS_TIME] << " s" << endl;
}

void Min_KW::output_RAM(ostream& os) const
{
    os << endl 
       << "RAM of " << a_.get_Name() << " (" << stat_.u_[RAM_ROWS] << "x" << stat_.u_[RAM_COLUMNS] << ")" << endl;
    print_RAM_TXT(os);

    if (param_.verbosity_ > 1)
    {
        os << endl
           << "LaTeX:" << endl;
        print_RAM_LaTeX(os);
    }

    os << endl
       << "time = " << stat_.d_[RAM_TIME] << " s" << endl; 
}

void Min_KW::output_Cover(ostream& os, Subset const& s) const
{
    print_Grids_Set_TXT(os, s);

    if (param_.verbosity_ > 1)
    {
        os << endl
           << "LaTeX:" << endl
           << endl;
        print_Grids_Set_LaTeX(os, s);
    }
}

void Min_KW::output_CM(ostream& os, Subset_Matrix const& cm) const
{
    os << endl 
       << "CM of " << a_.get_Name() << " (" << stat_.u_[RAM_ROWS] << "x" << stat_.u_[RAM_COLUMNS] << ")" << endl;
    print_CM_TXT(os, cm);

    if (param_.verbosity_ > 1)
    {
        os << endl
           << "LaTeX:" << endl;
        print_CM_LaTeX(os, cm);
    }
}

/* ================================================================================= */
/* Processing and printing statistics                                                */
/* ================================================================================= */

void kw::CalcStatD(vector<KW_Statistics> const& vkws, D_KW_Stat const& elem, double& d_min, double& d_max, double& mean, double& dev)
{
    u_t n = vkws.size();
    d_min = vkws[0].d_[elem];
    d_max = vkws[0].d_[elem];
    mean  = vkws[0].d_[elem];
    dev   = vkws[0].d_[elem] * vkws[0].d_[elem];

    for (u_t i = 1; i < n; ++i)
    {
        d_min = min(d_min, vkws[i].d_[elem]);
        d_max = max(d_max, vkws[i].d_[elem]);
        mean  += vkws[i].d_[elem];
        dev   += vkws[i].d_[elem] * vkws[i].d_[elem];
    }

    mean /= n;
    dev = sqrt(dev/n - mean * mean);
}

void kw::CalcStatU(vector<KW_Statistics> const& vkws, U_KW_Stat const& elem, u_t& u_min, u_t& u_max, double& mean, double& dev)
{
	u_t n = vkws.size();

	if (elem != MIN_STATES)
	{
		u_min = vkws[0].u_[elem];
		u_max = vkws[0].u_[elem];
		mean  = vkws[0].u_[elem];
		dev   = vkws[0].u_[elem] * vkws[0].u_[elem];

		for (u_t i = 1; i < n; ++i)
		{
			u_min = min(u_min, vkws[i].u_[elem]);
			u_max = max(u_max, vkws[i].u_[elem]);
			mean  += vkws[i].u_[elem];
			dev   += vkws[i].u_[elem] * vkws[i].u_[elem];
		}

		mean /= n;
		dev = sqrt(dev/n - mean * mean);
	}
	else
	{
		u_min = 0;
		u_max = 0;
		mean  = 0;
		dev   = 0;

		for (u_t i = 0; i < n; ++i)
		{
			if (vkws[i].u_[MIN_COUNT] > 0)
			{
				u_min = vkws[i].u_[elem];
				u_max = vkws[i].u_[elem];
				break;
			}
		}

		for (u_t i = 0; i < n; ++i)
		{
			if (vkws[i].u_[MIN_COUNT] > 0)
			{
				u_min = min(u_min, vkws[i].u_[elem]);
				u_max = max(u_max, vkws[i].u_[elem]);
				mean  += vkws[i].u_[elem];
				dev   += vkws[i].u_[elem] * vkws[i].u_[elem];
			}
		}

		u_t m;
		CalcSumB(vkws, UNMINIMIZED, m);
		n -= m;

		mean /= n;
		dev = sqrt(dev/n - mean * mean);
	}
}

void kw::CalcSumD(vector<KW_Statistics> const& vkws, D_KW_Stat const& elem, double& sum)
{
    sum = 0;
    for (u_t i = 0; i < vkws.size(); ++i)
    {
        sum += vkws[i].d_[elem];
    }
}

void kw::CalcSumU(vector<KW_Statistics> const& vkws, U_KW_Stat const& elem, u_t& sum)
{
    sum = 0;
    for (u_t i = 0; i < vkws.size(); ++i)
    {
        sum += vkws[i].u_[elem];
    }
}

void kw::CalcSumB(vector<KW_Statistics> const& vkws, B_KW_Stat const& elem, u_t& sum)
{
    sum = 0;
    for (u_t i = 0; i < vkws.size(); ++i)
    {
        sum += ( vkws[i].b_[elem] ? 1 : 0);
    }
}

void kw::OutputStatD(ostream& os, string const& name, vector<KW_Statistics> const& vkws, D_KW_Stat const& elem)
{
    double min, max, mean, dev;

    CalcStatD(vkws, elem, min, max, mean, dev);
    os << fixed << setprecision (4) << setw(40) << name << setw(15) << min << setw(15) << max << setw(15) << mean << setw(15) << dev << endl;
}

void kw::OutputStatU(ostream& os, string const& name, vector<KW_Statistics> const& vkws, U_KW_Stat const& elem)
{
    u_t min, max;
    double mean, dev;

    CalcStatU(vkws, elem, min, max, mean, dev);
    os << fixed << setprecision (4) << setw(40) << name << setw(15) << min << setw(15) << max << setw(15) << mean << setw(15) << dev << endl;
}

void kw::OutputSumD(ostream& os, string const& name, vector<KW_Statistics> const& vkws, D_KW_Stat const& elem)
{
    double sum;

    CalcSumD(vkws, elem, sum);
    os << name << sum << endl;
}

void kw::OutputSumU(ostream& os, string const& name, vector<KW_Statistics> const& vkws, U_KW_Stat const& elem)
{
    u_t sum;

    CalcSumU(vkws, elem, sum);
    os << name << sum << endl;
}

void kw::OutputSumB(ostream& os, string const& name, vector<KW_Statistics> const& vkws, B_KW_Stat const& elem)
{
    u_t sum;

    CalcSumB(vkws, elem, sum);
    os << name << sum << endl;
}

void kw::ProcessKWStatistics(ostream& os, vector<KW_Statistics> const& vkws)
{
    os << setw(40) << "Parameter" << setw(15) << "Min" << setw(15) << "Max" << setw(15) << "Mean" << setw(15) << "Stand. dev." << endl;
    
    PrintLine(os, 100, '=');

    OutputStatU(os, "States in A", vkws, A_STATES);
    OutputStatU(os, "States in D(A)", vkws, DA_STATES);
    OutputStatU(os, "States in M(D(A))", vkws, MDA_STATES);
    OutputStatU(os, "States in D(R(A))", vkws, DRA_STATES);
    OutputStatU(os, "States in M(D(R(A)))", vkws, MDRA_STATES);

    OutputStatU(os, "Rows in RAM", vkws, RAM_ROWS);
    OutputStatU(os, "Columns in RAM", vkws, RAM_COLUMNS);
    OutputStatU(os, "Size of RAM (rows*columns)", vkws, RAM_SIZE);
    OutputStatU(os, "Number of 1s in RAM", vkws, RAM_ONES_COUNT);
    OutputStatD(os, "Density of ones in RAM", vkws, RAM_ONES_DENSITY);
    OutputStatU(os, "Grids in RAM", vkws, GRIDS_COUNT);
    OutputStatU(os, "Fixed grids", vkws, FIXED_COUNT);

    OutputStatU(os, "Number of minimal automata", vkws, MIN_COUNT);
    OutputStatU(os, "States in minimal automata", vkws, MIN_STATES);

    OutputStatD(os, "Grids time (sec)", vkws, GRIDS_TIME);
    OutputStatD(os, "Search time (sec)", vkws, SEARCH_TIME);
    OutputStatD(os, "GA time (sec)", vkws, GA_TIME);
    OutputStatD(os, "SA time (sec)", vkws, SA_TIME);
    OutputStatD(os, "SHC time (sec)", vkws, SHC_TIME);
    OutputStatD(os, "Covers time (sec)", vkws, COVERS_TIME);
    OutputStatD(os, "Total time (sec)", vkws, TOTAL_TIME);

    PrintLine(os, 100, '=');

    os << endl 
       << "Overall statistics" << endl;
    PrintLine(os, 18, '=');

    os << "Automata processed: " << vkws.size() << endl;
    OutputSumU(os, "Minimal automata found: ", vkws, MIN_COUNT);
    OutputSumB(os, "Unminimized automata: ", vkws, UNMINIMIZED);
    OutputSumB(os, "Automata with minimal automaton equal to canonical automaton: ", vkws, MIN_MDA);
    OutputSumB(os, "Automata with inequivalent minimal covering automata: ", vkws, ILLEG_MIN_COVERS);
    OutputSumD(os, "Overall time (sec): ", vkws, TOTAL_TIME);
}


//EOF!
